$\forall$$A$,$B$:Type. strong{-}subtype($A$; $B$) $\in$ prop\{i:l\}